Nuprl Lemma : R-rframe-rule
0,22
postcript
pdf
i
,
x
:Id,
L
:Knd List. @
i
: only members of
L
read
x
||-
es
.@
i
: only members of
L
read
x
latex
Definitions
es
realizer
ind
Rrframe
compseq
tag
def
,
Consistent(
R
;
es
)
,
ES
,
t
T
,
x
:
A
.
B
(
x
)
,
@
loc
: only members of
L
read
x
,
@
i
: only members of
L
read
x
,
x
:
A
B
(
x
)
,
P
Q
,
True
,
R-Feasible(
R
)
,
inr(
x
)
,
x
:
A
B
(
x
)
,
P
&
Q
,
R
||-
es
.
P
(
es
)
,
Id
,
Knd
,
type
List
Lemmas
Knd
wf
,
Id
wf
,
R-consistent
wf
,
Rrframe
wf
,
event
system
wf
origin
i, x:Id, L:Knd List. @i: only members of L read x ||- es.@i: only members of L read x i, x:Id, L:Knd List. @i: only members of L read x ||- es.@i: only members of L read x 
T
B(x)
Q
B(x)